A:Type, B, C:(AType), eq:EqDecider(A), f:a:A fp B(a), g:a:A fp C(a), x:A, P:(a:AB(a)),
Q:(a:AC(a)).
(x:A. (x  dom(g))  (x  dom(f))  ((C(x) r B(x)) c (P(x,g(x))  Q(x,g(x)))))
 {g  f  (z != f(x)  P(y,z))  (z != g(x)  Q(y,z))} 

latex

Definitions	x:A. B(x), x(s), , P  Q, A c B, x(s1,s2), {T}, f  g, z != f(x)  P(a;z), t  T, x. t(x)
Lemmas	assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf-ap wf, fpf wf, deq wf